(declare-fun b () Real)
(declare-fun Jsnkj_new () Real)
(declare-fun t () Real)
(declare-fun f () Real)
(declare-fun g () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun l () Real)
(declare-fun k () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun t17uscore0dollarskuscore1_shifted () Real)
(assert (not (=> (or (=> (< 0.0) (or (<= 0.0 (+ (- k))) (<= m n 40 (div 249 b i)))) (< (+ (+ g (mod 0 (* 2.0))) (/ (+ (- (- j) (- Jsnkj_new l)) 1.0) (+ (+ (* (div 113)) (- t m))))) (+ 37 f o)) (<= 0.0 (- t m)) (< 0.0 (- Jsnkj_new l)) (< 0.0 (div 63 b i))) (< (- f o) (/ (- 1 2) (+ (/ t17uscore0dollarskuscore1_shifted (- t m))))) (< (- (+ (* (- l) t17uscore0dollarskuscore1_shifted) g) (div (* (+ (* l t17uscore0dollarskuscore1_shifted) (- t m)) (+ (* (/ (- 1.0) (/ 117 Jsnkj_new l)) t17uscore0dollarskuscore1_shifted) (- t m))) (* 2.0 (- Jsnkj_new)))) (- 11)))))
(check-sat)
